\begin{tabbing}
update{-}spec(${\it ds}$; ${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf(\=(:Knd $\times$ Id);\+
\\[0ex]${\it kz}$.(($n$:$\mathbb{N}$
\\[0ex]$\times$ \=(decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; (${\it kz}$.1))$\rightarrow$fpf{-}cap\+
\\[0ex](${\it ds}$; id{-}deq; (${\it kz}$.2); void))) List))
\-\-
\end{tabbing}